Skip to content

feat(Algebra/Polynomial/Splits): generalize Splits.of_splits_map to injective ring homomorphisms #34048

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Open
tb65536 wants to merge 1 commit into
base: master
Choose a base branch
from
Open

feat(Algebra/Polynomial/Splits): generalize Splits.of_splits_map to injective ring homomorphisms #34048

tb65536 wants to merge 1 commit into from
+10 −4

Conversation

@tb65536
Copy link
Collaborator

@tb65536 tb65536 commented Jan 16, 2026

This PR generalizes Splits.of_splits_map to injective ring homomorphisms.

Open in Gitpod

@tb65536 tb65536 added awaiting-CI This PR doesn't pass CI yet. This label is automatically removed once it does. t-algebra Algebra (groups, rings, fields, etc) t-ring-theory Ring theory labels Jan 16, 2026
@github-actions
Copy link

github-actions bot commented Jan 16, 2026

PR summary 2b4c6152f1

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ Splits.of_splits_map_of_injective

You can run this locally as follows 
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@github-actions github-actions bot removed the awaiting-CI This PR doesn't pass CI yet. This label is automatically removed once it does. label Jan 16, 2026
erdOne
erdOne reviewed Jan 18, 2026
View reviewed changes
Copy link
Member

@erdOne erdOne left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks!
maintainer merge

@github-actions
Copy link

github-actions bot commented Jan 18, 2026

🚀 Pull request has been placed on the maintainer queue by erdOne.

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jan 18, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@erdOne erdOne erdOne left review comments

Assignees

No one assigned

Labels

maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. t-algebra Algebra (groups, rings, fields, etc) t-ring-theory Ring theory

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@tb65536 @erdOne @leanprover-community-mathlib4-bot